Left Termination proof of /tmp/tmpJzk0F6/btapplast.pl

Left Termination of the query pattern
goal(g,a,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 281 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 128 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 331 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇒, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔, 0 ms)

        ↳25 PiDP

        ↳26 PiDPToQDPProof (⇒, 0 ms)

        ↳27 QDP

        ↳28 QDPSizeChangeProof (⇔, 0 ms)

        ↳29 YES

(0) Obligation:

Clauses:

goal(A, B, C) :- ','(s2t(A, T), tapplast(T, B, C)).
tapplast(L, X, Last) :- ','(tappend(L, node(nil, X, nil), LX), tlast(Last, LX)).
tlast(X, node(nil, X, nil)).
tlast(X, node(L, H, R)) :- tlast(X, L).
tlast(X, node(L, H, R)) :- tlast(X, R).
tappend(nil, T, T).
tappend(node(nil, X, T2), T1, node(T1, X, T2)).
tappend(node(T1, X, nil), T2, node(T1, X, T2)).
tappend(node(T1, X, T2), T3, node(U, X, T2)) :- tappend(T1, T3, U).
tappend(node(T1, X, T2), T3, node(T1, X, U)) :- tappend(T2, T3, U).
s2t(s(X), node(T, Y, T)) :- s2t(X, T).
s2t(s(X), node(nil, Y, T)) :- s2t(X, T).
s2t(s(X), node(T, Y, nil)) :- s2t(X, T).
s2t(s(X), node(nil, Y, nil)).
s2t(0, nil).

Query: goal(g,a,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: goal(T4, T5, T6)\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: goal(T4, T5, T6), SCOPE: 1, CLAUSE: 0\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(s2t(T10, X7), tapplast(X7, T13, T14))\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 10 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 11 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 10\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 11 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(s2t(T19, X31), tapplast(node(X31, X32, X31), T13, T14))\n\nT19 is ground\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: s2t(T19, X31)\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: tapplast(node(T21, X32, T21), T13, T14)\n\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: s2t(T19, X31), SCOPE: 3, CLAUSE: 10 | s2t(T19, X31), SCOPE: 3, CLAUSE: 11 | s2t(T19, X31), SCOPE: 3, CLAUSE: 12 | s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: s2t(T19, X31), SCOPE: 3, CLAUSE: 10\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: s2t(T19, X31), SCOPE: 3, CLAUSE: 11 | s2t(T19, X31), SCOPE: 3, CLAUSE: 12 | s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: s2t(T27, X66)\n\nT27 is ground\nX66 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: s2t(T19, X31), SCOPE: 3, CLAUSE: 11\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: s2t(T19, X31), SCOPE: 3, CLAUSE: 12 | s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: s2t(T33, X97)\n\nT33 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: s2t(T19, X31), SCOPE: 3, CLAUSE: 12\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: s2t(T39, X126)\n\nT39 is ground\nX126 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: s2t(T19, X31), SCOPE: 3, CLAUSE: 13\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: tapplast(node(T21, X32, T21), T13, T14), SCOPE: 4, CLAUSE: 1\n\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(tappend(node(T61, X168, T61), node(nil, T62, nil), X167), tlast(T63, X167))\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: tappend(node(T61, X168, T61), node(nil, T62, nil), X167)\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: tlast(T66, T65)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 5 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 6 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 7 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 8 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 9\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 6 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 7 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 8 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 9\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 6\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 7 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 8 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 9\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 7\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 8 | tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 9\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 8\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: tappend(node(T61, X168, T61), node(nil, T62, nil), X167), SCOPE: 5, CLAUSE: 9\n\nX168 is free\nX167 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: tappend(T100, node(nil, T101, nil), X252)\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 5 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 6 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 7 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 8 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 9\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 5\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 6 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 7 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 8 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 9\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 6\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 7 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 8 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 9\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 7\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 8 | tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 9\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 8\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: tappend(T100, node(nil, T101, nil), X252), SCOPE: 6, CLAUSE: 9\n\nX252 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: tappend(T159, node(nil, T160, nil), X319)\n\nX319 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: tappend(T175, node(nil, T176, nil), X339)\n\nX339 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: tappend(T189, node(nil, T190, nil), X364)\n\nX364 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: tlast(T66, T65), SCOPE: 7, CLAUSE: 2 | tlast(T66, T65), SCOPE: 7, CLAUSE: 3 | tlast(T66, T65), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: tlast(T66, T65), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: tlast(T66, T65), SCOPE: 7, CLAUSE: 3 | tlast(T66, T65), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: tlast(T66, T65), SCOPE: 7, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: tlast(T66, T65), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: tlast(T220, T221)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: tlast(T236, T237)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 11\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(s2t(T244, X434), tapplast(node(nil, X433, X434), T13, T14))\n\nT244 is ground\nX433 is free\nX434 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: s2t(T244, X434)\n\nT244 is ground\nX434 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: tapplast(node(nil, X433, T246), T13, T14)\n\nX433 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: tapplast(node(nil, X433, T246), T13, T14), SCOPE: 8, CLAUSE: 1\n\nX433 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(tappend(node(nil, X465, T263), node(nil, T264, nil), X464), tlast(T265, X464))\n\nX465 is free\nX464 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: tappend(node(nil, X465, T263), node(nil, T264, nil), X464)\n\nX465 is free\nX464 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: tlast(T268, T267)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(s2t(T275, X495), tapplast(node(X495, X496, nil), T13, T14))\n\nT275 is ground\nX495 is free\nX496 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: s2t(T275, X495)\n\nT275 is ground\nX495 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: tapplast(node(T277, X496, nil), T13, T14)\n\nX496 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: tapplast(node(T277, X496, nil), T13, T14), SCOPE: 9, CLAUSE: 1\n\nX496 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(tappend(node(T294, X527, nil), node(nil, T295, nil), X526), tlast(T296, X526))\n\nX527 is free\nX526 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: tappend(node(T294, X527, nil), node(nil, T295, nil), X526)\n\nX527 is free\nX526 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: tlast(T299, T298)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: tapplast(node(nil, X548, nil), T13, T14)\n\nX548 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: tapplast(node(nil, X548, nil), T13, T14), SCOPE: 10, CLAUSE: 1\n\nX548 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(tappend(node(nil, X569, nil), node(nil, T317, nil), X568), tlast(T318, X568))\n\nX569 is free\nX568 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: tapplast(nil, T13, T14)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: tapplast(nil, T13, T14), SCOPE: 11, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(tappend(nil, node(nil, T331, nil), X588), tlast(T332, X588))\n\nX588 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: tappend(nil, node(nil, T331, nil), X588)\n\nX588 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: tlast(T336, T335)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 118 [arrowhead = none ];
118 -> 2;

119 [label="ONLY EVAL with clause\ngoal(X4, X5, X6) :- ','(s2t(X4, X7), tapplast(X7, X5, X6)).\nand substitutionT4 -> T10,\nX4 -> T10,\nT5 -> T13,\nX5 -> T13,\nT6 -> T14,\nX6 -> T14,\nT11 -> T13,\nT12 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 119 [arrowhead = none ];
119 -> 3;

120 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 120 [arrowhead = none ];
120 -> 4;

121 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 121 [arrowhead = none ];
121 -> 5;

122 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 122 [arrowhead = none ];
122 -> 6;

123 [label="EVAL with clause\ns2t(s(X28), node(X29, X30, X29)) :- s2t(X28, X29).\nand substitutionX28 -> T19,\nT10 -> s(T19),\nX29 -> X31,\nX30 -> X32,\nX7 -> node(X31, X32, X31)", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 123 [arrowhead = none ];
123 -> 7;

124 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 124 [arrowhead = none ];
124 -> 8;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 125 [arrowhead = none ];
125 -> 86;

126 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 126 [arrowhead = none ];
126 -> 87;

127 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
7 -> 127 [arrowhead = none ];
127 -> 9;

128 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nreplacements:X31 -> T21", fontsize=14, style = filled, fillcolor = violet];
7 -> 128 [arrowhead = none ];
128 -> 10;

129 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
9 -> 129 [arrowhead = none ];
129 -> 11;

130 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 130 [arrowhead = none ];
130 -> 32;

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 131 [arrowhead = none ];
131 -> 12;

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 132 [arrowhead = none ];
132 -> 13;

133 [label="EVAL with clause\ns2t(s(X63), node(X64, X65, X64)) :- s2t(X63, X64).\nand substitutionX63 -> T27,\nT19 -> s(T27),\nX64 -> X66,\nX65 -> X67,\nX31 -> node(X66, X67, X66)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 133 [arrowhead = none ];
133 -> 14;

134 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 134 [arrowhead = none ];
134 -> 15;

135 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 135 [arrowhead = none ];
135 -> 16;

136 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 136 [arrowhead = none ];
136 -> 17;

137 [label="INSTANCE with matching:\nT19 -> T27\nX31 -> X66", fontsize=14, style = filled, fillcolor = lightgrey];
14 -> 137 [arrowhead = none , style=dashed];
137 -> 9[style=dashed];

138 [label="EVAL with clause\ns2t(s(X93), node(nil, X94, X95)) :- s2t(X93, X95).\nand substitutionX93 -> T33,\nT19 -> s(T33),\nX94 -> X96,\nX95 -> X97,\nX31 -> node(nil, X96, X97)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 138 [arrowhead = none ];
138 -> 18;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 139 [arrowhead = none ];
139 -> 19;

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
17 -> 140 [arrowhead = none ];
140 -> 20;

141 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
17 -> 141 [arrowhead = none ];
141 -> 21;

142 [label="INSTANCE with matching:\nT19 -> T33\nX31 -> X97", fontsize=14, style = filled, fillcolor = lightgrey];
18 -> 142 [arrowhead = none , style=dashed];
142 -> 9[style=dashed];

143 [label="EVAL with clause\ns2t(s(X123), node(X124, X125, nil)) :- s2t(X123, X124).\nand substitutionX123 -> T39,\nT19 -> s(T39),\nX124 -> X126,\nX125 -> X127,\nX31 -> node(X126, X127, nil)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 143 [arrowhead = none ];
143 -> 22;

144 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 144 [arrowhead = none ];
144 -> 23;

145 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 145 [arrowhead = none ];
145 -> 24;

146 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 146 [arrowhead = none ];
146 -> 25;

147 [label="INSTANCE with matching:\nT19 -> T39\nX31 -> X126", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 147 [arrowhead = none , style=dashed];
147 -> 9[style=dashed];

148 [label="EVAL with clause\ns2t(s(X145), node(nil, X146, nil)).\nand substitutionX145 -> T45,\nT19 -> s(T45),\nX146 -> X147,\nX31 -> node(nil, X147, nil)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 148 [arrowhead = none ];
148 -> 26;

149 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 149 [arrowhead = none ];
149 -> 27;

150 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT19 -> 0,\nX31 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 150 [arrowhead = none ];
150 -> 29;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 151 [arrowhead = none ];
151 -> 30;

152 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 152 [arrowhead = none ];
152 -> 28;

153 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 153 [arrowhead = none ];
153 -> 31;

154 [label="ONLY EVAL with clause\ntapplast(X164, X165, X166) :- ','(tappend(X164, node(nil, X165, nil), X167), tlast(X166, X167)).\nand substitutionT21 -> T61,\nX32 -> X168,\nX164 -> node(T61, X168, T61),\nT13 -> T62,\nX165 -> T62,\nT14 -> T63,\nX166 -> T63,\nT58 -> T61,\nT59 -> T62,\nT60 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 154 [arrowhead = none ];
154 -> 33;

155 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
33 -> 155 [arrowhead = none ];
155 -> 34;

156 [label="SPLIT 2\nreplacements:X168 -> T64,\nX167 -> T65,\nT63 -> T66", fontsize=14, style = filled, fillcolor = violet];
33 -> 156 [arrowhead = none ];
156 -> 35;

157 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 157 [arrowhead = none ];
157 -> 36;

158 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 158 [arrowhead = none ];
158 -> 74;

159 [label="BACKTRACK\nfor clause: tappend(nil, T, T)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 159 [arrowhead = none ];
159 -> 37;

160 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 160 [arrowhead = none ];
160 -> 38;

161 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 161 [arrowhead = none ];
161 -> 39;

162 [label="EVAL with clause\ntappend(node(nil, X190, X191), X192, node(X192, X190, X191)).\nand substitutionT61 -> nil,\nX168 -> X193,\nX190 -> X193,\nX191 -> nil,\nT62 -> T71,\nX192 -> node(nil, T71, nil),\nX167 -> node(node(nil, T71, nil), X193, nil)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 162 [arrowhead = none ];
162 -> 40;

163 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 163 [arrowhead = none ];
163 -> 41;

164 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 164 [arrowhead = none ];
164 -> 43;

165 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 165 [arrowhead = none ];
165 -> 44;

166 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 166 [arrowhead = none ];
166 -> 42;

167 [label="EVAL with clause\ntappend(node(X210, X211, nil), X212, node(X210, X211, X212)).\nand substitutionT61 -> nil,\nX210 -> nil,\nX168 -> X213,\nX211 -> X213,\nT80 -> nil,\nT62 -> T81,\nX212 -> node(nil, T81, nil),\nX167 -> node(nil, X213, node(nil, T81, nil))", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 167 [arrowhead = none ];
167 -> 45;

168 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 168 [arrowhead = none ];
168 -> 46;

169 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 169 [arrowhead = none ];
169 -> 48;

170 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 170 [arrowhead = none ];
170 -> 49;

171 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 171 [arrowhead = none ];
171 -> 47;

172 [label="ONLY EVAL with clause\ntappend(node(X246, X247, X248), X249, node(X250, X247, X248)) :- tappend(X246, X249, X250).\nand substitutionT61 -> T100,\nX246 -> T100,\nX168 -> X251,\nX247 -> X251,\nX248 -> T100,\nT62 -> T101,\nX249 -> node(nil, T101, nil),\nX250 -> X252,\nX167 -> node(X252, X251, T100),\nT98 -> T100,\nT99 -> T101", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 172 [arrowhead = none ];
172 -> 50;

173 [label="ONLY EVAL with clause\ntappend(node(X358, X359, X360), X361, node(X358, X359, X362)) :- tappend(X360, X361, X362).\nand substitutionT61 -> T189,\nX358 -> T189,\nX168 -> X363,\nX359 -> X363,\nX360 -> T189,\nT62 -> T190,\nX361 -> node(nil, T190, nil),\nX362 -> X364,\nX167 -> node(T189, X363, X364),\nT187 -> T189,\nT188 -> T190", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 173 [arrowhead = none ];
173 -> 73;

174 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 174 [arrowhead = none ];
174 -> 51;

175 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 175 [arrowhead = none ];
175 -> 52;

176 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 176 [arrowhead = none ];
176 -> 53;

177 [label="EVAL with clause\ntappend(nil, X259, X259).\nand substitutionT100 -> nil,\nT101 -> T108,\nX259 -> node(nil, T108, nil),\nX252 -> node(nil, T108, nil)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 177 [arrowhead = none ];
177 -> 54;

178 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 178 [arrowhead = none ];
178 -> 55;

179 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 179 [arrowhead = none ];
179 -> 57;

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 180 [arrowhead = none ];
180 -> 58;

181 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 181 [arrowhead = none ];
181 -> 56;

182 [label="EVAL with clause\ntappend(node(nil, X272, X273), X274, node(X274, X272, X273)).\nand substitutionX272 -> T121,\nX273 -> T122,\nT100 -> node(nil, T121, T122),\nT101 -> T123,\nX274 -> node(nil, T123, nil),\nX252 -> node(node(nil, T123, nil), T121, T122)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 182 [arrowhead = none ];
182 -> 59;

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 183 [arrowhead = none ];
183 -> 60;

184 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 184 [arrowhead = none ];
184 -> 62;

185 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 185 [arrowhead = none ];
185 -> 63;

186 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 186 [arrowhead = none ];
186 -> 61;

187 [label="EVAL with clause\ntappend(node(X287, X288, nil), X289, node(X287, X288, X289)).\nand substitutionX287 -> T136,\nX288 -> T137,\nT100 -> node(T136, T137, nil),\nT101 -> T138,\nX289 -> node(nil, T138, nil),\nX252 -> node(T136, T137, node(nil, T138, nil))", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 187 [arrowhead = none ];
187 -> 64;

188 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 188 [arrowhead = none ];
188 -> 65;

189 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
63 -> 189 [arrowhead = none ];
189 -> 67;

190 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
63 -> 190 [arrowhead = none ];
190 -> 68;

191 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 191 [arrowhead = none ];
191 -> 66;

192 [label="EVAL with clause\ntappend(node(X314, X315, X316), X317, node(X318, X315, X316)) :- tappend(X314, X317, X318).\nand substitutionX314 -> T159,\nX315 -> T156,\nX316 -> T157,\nT100 -> node(T159, T156, T157),\nT101 -> T160,\nX317 -> node(nil, T160, nil),\nX318 -> X319,\nX252 -> node(X319, T156, T157),\nT155 -> T159,\nT158 -> T160", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 192 [arrowhead = none ];
192 -> 69;

193 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 193 [arrowhead = none ];
193 -> 70;

194 [label="EVAL with clause\ntappend(node(X334, X335, X336), X337, node(X334, X335, X338)) :- tappend(X336, X337, X338).\nand substitutionX334 -> T171,\nX335 -> T172,\nX336 -> T175,\nT100 -> node(T171, T172, T175),\nT101 -> T176,\nX337 -> node(nil, T176, nil),\nX338 -> X339,\nX252 -> node(T171, T172, X339),\nT173 -> T175,\nT174 -> T176", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 194 [arrowhead = none ];
194 -> 71;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 195 [arrowhead = none ];
195 -> 72;

196 [label="INSTANCE with matching:\nT100 -> T159\nT101 -> T160\nX252 -> X319", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 196 [arrowhead = none , style=dashed];
196 -> 50[style=dashed];

197 [label="INSTANCE with matching:\nT100 -> T175\nT101 -> T176\nX252 -> X339", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 197 [arrowhead = none , style=dashed];
197 -> 50[style=dashed];

198 [label="INSTANCE with matching:\nT100 -> T189\nT101 -> T190\nX252 -> X364", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 198 [arrowhead = none , style=dashed];
198 -> 50[style=dashed];

199 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 199 [arrowhead = none ];
199 -> 75;

200 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 200 [arrowhead = none ];
200 -> 76;

201 [label="EVAL with clause\ntlast(X373, node(nil, X373, nil)).\nand substitutionT66 -> T199,\nX373 -> T199,\nT65 -> node(nil, T199, nil)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 201 [arrowhead = none ];
201 -> 77;

202 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 202 [arrowhead = none ];
202 -> 78;

203 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 203 [arrowhead = none ];
203 -> 80;

204 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 204 [arrowhead = none ];
204 -> 81;

205 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 205 [arrowhead = none ];
205 -> 79;

206 [label="EVAL with clause\ntlast(X390, node(X391, X392, X393)) :- tlast(X390, X391).\nand substitutionT66 -> T220,\nX390 -> T220,\nX391 -> T221,\nX392 -> T218,\nX393 -> T219,\nT65 -> node(T221, T218, T219),\nT216 -> T220,\nT217 -> T221", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 206 [arrowhead = none ];
206 -> 82;

207 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 207 [arrowhead = none ];
207 -> 83;

208 [label="EVAL with clause\ntlast(X404, node(X405, X406, X407)) :- tlast(X404, X407).\nand substitutionT66 -> T236,\nX404 -> T236,\nX405 -> T233,\nX406 -> T234,\nX407 -> T237,\nT65 -> node(T233, T234, T237),\nT232 -> T236,\nT235 -> T237", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 208 [arrowhead = none ];
208 -> 84;

209 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 209 [arrowhead = none ];
209 -> 85;

210 [label="INSTANCE with matching:\nT66 -> T220\nT65 -> T221", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 210 [arrowhead = none , style=dashed];
210 -> 35[style=dashed];

211 [label="INSTANCE with matching:\nT66 -> T236\nT65 -> T237", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 211 [arrowhead = none , style=dashed];
211 -> 35[style=dashed];

212 [label="EVAL with clause\ns2t(s(X430), node(nil, X431, X432)) :- s2t(X430, X432).\nand substitutionX430 -> T244,\nT10 -> s(T244),\nX431 -> X433,\nX432 -> X434,\nX7 -> node(nil, X433, X434)", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 212 [arrowhead = none ];
212 -> 88;

213 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 213 [arrowhead = none ];
213 -> 89;

214 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 214 [arrowhead = none ];
214 -> 96;

215 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 215 [arrowhead = none ];
215 -> 97;

216 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
88 -> 216 [arrowhead = none ];
216 -> 90;

217 [label="SPLIT 2\nnew knowledge:\nT244 is ground\nreplacements:X434 -> T246", fontsize=14, style = filled, fillcolor = violet];
88 -> 217 [arrowhead = none ];
217 -> 91;

218 [label="INSTANCE with matching:\nT19 -> T244\nX31 -> X434", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 218 [arrowhead = none , style=dashed];
218 -> 9[style=dashed];

219 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 219 [arrowhead = none ];
219 -> 92;

220 [label="ONLY EVAL with clause\ntapplast(X461, X462, X463) :- ','(tappend(X461, node(nil, X462, nil), X464), tlast(X463, X464)).\nand substitutionX433 -> X465,\nT246 -> T263,\nX461 -> node(nil, X465, T263),\nT13 -> T264,\nX462 -> T264,\nT14 -> T265,\nX463 -> T265,\nT260 -> T263,\nT261 -> T264,\nT262 -> T265", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 220 [arrowhead = none ];
220 -> 93;

221 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
93 -> 221 [arrowhead = none ];
221 -> 94;

222 [label="SPLIT 2\nreplacements:X465 -> T266,\nX464 -> T267,\nT265 -> T268", fontsize=14, style = filled, fillcolor = violet];
93 -> 222 [arrowhead = none ];
222 -> 95;

223 [label="INSTANCE with matching:\nT100 -> node(nil, X465, T263)\nT101 -> T264\nX252 -> X464", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 223 [arrowhead = none , style=dashed];
223 -> 50[style=dashed];

224 [label="INSTANCE with matching:\nT66 -> T268\nT65 -> T267", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 224 [arrowhead = none , style=dashed];
224 -> 35[style=dashed];

225 [label="EVAL with clause\ns2t(s(X492), node(X493, X494, nil)) :- s2t(X492, X493).\nand substitutionX492 -> T275,\nT10 -> s(T275),\nX493 -> X495,\nX494 -> X496,\nX7 -> node(X495, X496, nil)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 225 [arrowhead = none ];
225 -> 98;

226 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 226 [arrowhead = none ];
226 -> 99;

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
97 -> 227 [arrowhead = none ];
227 -> 106;

228 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
97 -> 228 [arrowhead = none ];
228 -> 107;

229 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
98 -> 229 [arrowhead = none ];
229 -> 100;

230 [label="SPLIT 2\nnew knowledge:\nT275 is ground\nreplacements:X495 -> T277", fontsize=14, style = filled, fillcolor = violet];
98 -> 230 [arrowhead = none ];
230 -> 101;

231 [label="INSTANCE with matching:\nT19 -> T275\nX31 -> X495", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 231 [arrowhead = none , style=dashed];
231 -> 9[style=dashed];

232 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
101 -> 232 [arrowhead = none ];
232 -> 102;

233 [label="ONLY EVAL with clause\ntapplast(X523, X524, X525) :- ','(tappend(X523, node(nil, X524, nil), X526), tlast(X525, X526)).\nand substitutionT277 -> T294,\nX496 -> X527,\nX523 -> node(T294, X527, nil),\nT13 -> T295,\nX524 -> T295,\nT14 -> T296,\nX525 -> T296,\nT291 -> T294,\nT292 -> T295,\nT293 -> T296", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 233 [arrowhead = none ];
233 -> 103;

234 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
103 -> 234 [arrowhead = none ];
234 -> 104;

235 [label="SPLIT 2\nreplacements:X527 -> T297,\nX526 -> T298,\nT296 -> T299", fontsize=14, style = filled, fillcolor = violet];
103 -> 235 [arrowhead = none ];
235 -> 105;

236 [label="INSTANCE with matching:\nT100 -> node(T294, X527, nil)\nT101 -> T295\nX252 -> X526", fontsize=14, style = filled, fillcolor = lightgrey];
104 -> 236 [arrowhead = none , style=dashed];
236 -> 50[style=dashed];

237 [label="INSTANCE with matching:\nT66 -> T299\nT65 -> T298", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 237 [arrowhead = none , style=dashed];
237 -> 35[style=dashed];

238 [label="EVAL with clause\ns2t(s(X546), node(nil, X547, nil)).\nand substitutionX546 -> T306,\nT10 -> s(T306),\nX547 -> X548,\nX7 -> node(nil, X548, nil)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 238 [arrowhead = none ];
238 -> 108;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 239 [arrowhead = none ];
239 -> 109;

240 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT10 -> 0,\nX7 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 240 [arrowhead = none ];
240 -> 112;

241 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 241 [arrowhead = none ];
241 -> 113;

242 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
108 -> 242 [arrowhead = none ];
242 -> 110;

243 [label="ONLY EVAL with clause\ntapplast(X565, X566, X567) :- ','(tappend(X565, node(nil, X566, nil), X568), tlast(X567, X568)).\nand substitutionX548 -> X569,\nX565 -> node(nil, X569, nil),\nT13 -> T317,\nX566 -> T317,\nT14 -> T318,\nX567 -> T318,\nT315 -> T317,\nT316 -> T318", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 243 [arrowhead = none ];
243 -> 111;

244 [label="INSTANCE with matching:\nT61 -> nil\nX168 -> X569\nT62 -> T317\nX167 -> X568\nT63 -> T318", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 244 [arrowhead = none , style=dashed];
244 -> 33[style=dashed];

245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
112 -> 245 [arrowhead = none ];
245 -> 114;

246 [label="ONLY EVAL with clause\ntapplast(X585, X586, X587) :- ','(tappend(X585, node(nil, X586, nil), X588), tlast(X587, X588)).\nand substitutionX585 -> nil,\nT13 -> T331,\nX586 -> T331,\nT14 -> T332,\nX587 -> T332,\nT329 -> T331,\nT330 -> T332", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 246 [arrowhead = none ];
246 -> 115;

247 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
115 -> 247 [arrowhead = none ];
247 -> 116;

248 [label="SPLIT 2\nreplacements:X588 -> T335,\nT332 -> T336", fontsize=14, style = filled, fillcolor = violet];
115 -> 248 [arrowhead = none ];
248 -> 117;

249 [label="INSTANCE with matching:\nT100 -> nil\nT101 -> T331\nX252 -> X588", fontsize=14, style = filled, fillcolor = lightgrey];
116 -> 249 [arrowhead = none , style=dashed];
249 -> 50[style=dashed];

250 [label="INSTANCE with matching:\nT66 -> T336\nT65 -> T335", fontsize=14, style = filled, fillcolor = lightgrey];
117 -> 250 [arrowhead = none , style=dashed];
250 -> 35[style=dashed];

}

(2) Obligation:

Clauses:

s2tA(s(T27), node(X66, X67, X66)) :- s2tA(T27, X66).
s2tA(s(T33), node(nil, X96, X97)) :- s2tA(T33, X97).
s2tA(s(T39), node(X126, X127, nil)) :- s2tA(T39, X126).
s2tA(s(T45), node(nil, X147, nil)).
s2tA(0, nil).
tappendB(nil, T108, node(nil, T108, nil)).
tappendB(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)).
tappendB(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))).
tappendB(node(T159, T156, T157), T160, node(X319, T156, T157)) :- tappendB(T159, T160, X319).
tappendB(node(T171, T172, T175), T176, node(T171, T172, X339)) :- tappendB(T175, T176, X339).
tlastC(T199, node(nil, T199, nil)).
tlastC(T220, node(T221, T218, T219)) :- tlastC(T220, T221).
tlastC(T236, node(T233, T234, T237)) :- tlastC(T236, T237).
pD(T61, X168, T62, X167, T63) :- tappendE(T61, X168, T62, X167).
pD(T61, T64, T62, T65, T66) :- ','(tappendE(T61, T64, T62, T65), tlastC(T66, T65)).
tappendE(nil, X193, T71, node(node(nil, T71, nil), X193, nil)).
tappendE(nil, X213, T81, node(nil, X213, node(nil, T81, nil))).
tappendE(T100, X251, T101, node(X252, X251, T100)) :- tappendB(T100, T101, X252).
tappendE(T189, X363, T190, node(T189, X363, X364)) :- tappendB(T189, T190, X364).
goalF(s(T19), T13, T14) :- s2tA(T19, X31).
goalF(s(T19), T62, T63) :- ','(s2tA(T19, T61), pD(T61, X168, T62, X167, T63)).
goalF(s(T244), T13, T14) :- s2tA(T244, X434).
goalF(s(T244), T264, T265) :- ','(s2tA(T244, T263), tappendB(node(nil, X465, T263), T264, X464)).
goalF(s(T244), T264, T268) :- ','(s2tA(T244, T263), ','(tappendB(node(nil, T266, T263), T264, T267), tlastC(T268, T267))).
goalF(s(T275), T13, T14) :- s2tA(T275, X495).
goalF(s(T275), T295, T296) :- ','(s2tA(T275, T294), tappendB(node(T294, X527, nil), T295, X526)).
goalF(s(T275), T295, T299) :- ','(s2tA(T275, T294), ','(tappendB(node(T294, T297, nil), T295, T298), tlastC(T299, T298))).
goalF(s(T306), T317, T318) :- pD(nil, X569, T317, X568, T318).
goalF(0, T331, T332) :- tappendB(nil, T331, X588).
goalF(0, T331, T336) :- ','(tappendB(nil, T331, T335), tlastC(T336, T335)).

Query: goalF(g,a,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
goalF_in: (b,f,f)
s2tA_in: (b,f)
pD_in: (b,f,f,f,f)
tappendE_in: (b,f,f,f)
tappendB_in: (b,f,f)
tlastC_in: (f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOALF_IN_GAA(s(T19), T13, T14) → U13_GAA(T19, T13, T14, s2tA_in_ga(T19, X31))
GOALF_IN_GAA(s(T19), T13, T14) → S2TA_IN_GA(T19, X31)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → U1_GA(T27, X66, X67, s2tA_in_ga(T27, X66))
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → U2_GA(T33, X96, X97, s2tA_in_ga(T33, X97))
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → U3_GA(T39, X126, X127, s2tA_in_ga(T39, X126))
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)
GOALF_IN_GAA(s(T19), T62, T63) → U14_GAA(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_GAA(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → PD_IN_GAAAA(T61, X168, T62, X167, T63)
PD_IN_GAAAA(T61, X168, T62, X167, T63) → U8_GAAAA(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
PD_IN_GAAAA(T61, X168, T62, X167, T63) → TAPPENDE_IN_GAAA(T61, X168, T62, X167)
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → U11_GAAA(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → TAPPENDB_IN_GAA(T100, T101, X252)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_GAA(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_GAA(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → U12_GAAA(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → TAPPENDB_IN_GAA(T189, T190, X364)
PD_IN_GAAAA(T61, T64, T62, T65, T66) → U9_GAAAA(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_GAAAA(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → TLASTC_IN_AG(T66, T65)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → U6_AG(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)
TLASTC_IN_AG(T236, node(T233, T234, T237)) → U7_AG(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
GOALF_IN_GAA(s(T244), T13, T14) → U16_GAA(T244, T13, T14, s2tA_in_ga(T244, X434))
GOALF_IN_GAA(s(T244), T264, T265) → U17_GAA(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_GAA(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, X465, T263), T264, X464)
GOALF_IN_GAA(s(T244), T264, T268) → U19_GAA(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_GAA(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, T266, T263), T264, T267)
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_GAA(T244, T264, T268, tlastC_in_ag(T268, T267))
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → TLASTC_IN_AG(T268, T267)
GOALF_IN_GAA(s(T275), T13, T14) → U22_GAA(T275, T13, T14, s2tA_in_ga(T275, X495))
GOALF_IN_GAA(s(T275), T295, T296) → U23_GAA(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_GAA(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, X527, nil), T295, X526)
GOALF_IN_GAA(s(T275), T295, T299) → U25_GAA(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_GAA(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, T297, nil), T295, T298)
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_GAA(T275, T295, T299, tlastC_in_ag(T299, T298))
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → TLASTC_IN_AG(T299, T298)
GOALF_IN_GAA(s(T306), T317, T318) → U28_GAA(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
GOALF_IN_GAA(s(T306), T317, T318) → PD_IN_GAAAA(nil, X569, T317, X568, T318)
GOALF_IN_GAA(0, T331, T332) → U29_GAA(T331, T332, tappendB_in_gaa(nil, T331, X588))
GOALF_IN_GAA(0, T331, T332) → TAPPENDB_IN_GAA(nil, T331, X588)
GOALF_IN_GAA(0, T331, T336) → U30_GAA(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_GAA(T331, T336, tlastC_in_ag(T336, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → TLASTC_IN_AG(T336, T335)

The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

The argument filtering Pi contains the following mapping:
goalF_in_gaa(x1, x2, x3) = goalF_in_gaa(x1)
s(x1) = s(x1)
U13_gaa(x1, x2, x3, x4) = U13_gaa(x4)
s2tA_in_ga(x1, x2) = s2tA_in_ga(x1)
U1_ga(x1, x2, x3, x4) = U1_ga(x4)
U2_ga(x1, x2, x3, x4) = U2_ga(x4)
U3_ga(x1, x2, x3, x4) = U3_ga(x4)
s2tA_out_ga(x1, x2) = s2tA_out_ga(x2)
node(x1, x2, x3) = node(x1, x3)
0 = 0
goalF_out_gaa(x1, x2, x3) = goalF_out_gaa
U14_gaa(x1, x2, x3, x4) = U14_gaa(x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x4)
pD_in_gaaaa(x1, x2, x3, x4, x5) = pD_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6) = U8_gaaaa(x6)
tappendE_in_gaaa(x1, x2, x3, x4) = tappendE_in_gaaa(x1)
nil = nil
tappendE_out_gaaa(x1, x2, x3, x4) = tappendE_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5) = U11_gaaa(x1, x5)
tappendB_in_gaa(x1, x2, x3) = tappendB_in_gaa(x1)
tappendB_out_gaa(x1, x2, x3) = tappendB_out_gaa(x3)
U4_gaa(x1, x2, x3, x4, x5, x6) = U4_gaa(x3, x6)
U5_gaa(x1, x2, x3, x4, x5, x6) = U5_gaa(x1, x6)
U12_gaaa(x1, x2, x3, x4, x5) = U12_gaaa(x1, x5)
pD_out_gaaaa(x1, x2, x3, x4, x5) = pD_out_gaaaa(x4)
U9_gaaaa(x1, x2, x3, x4, x5, x6) = U9_gaaaa(x6)
U10_gaaaa(x1, x2, x3, x4, x5, x6) = U10_gaaaa(x4, x6)
tlastC_in_ag(x1, x2) = tlastC_in_ag(x2)
tlastC_out_ag(x1, x2) = tlastC_out_ag
U6_ag(x1, x2, x3, x4, x5) = U6_ag(x5)
U7_ag(x1, x2, x3, x4, x5) = U7_ag(x5)
U16_gaa(x1, x2, x3, x4) = U16_gaa(x4)
U17_gaa(x1, x2, x3, x4) = U17_gaa(x4)
U18_gaa(x1, x2, x3, x4) = U18_gaa(x4)
U19_gaa(x1, x2, x3, x4) = U19_gaa(x4)
U20_gaa(x1, x2, x3, x4) = U20_gaa(x4)
U21_gaa(x1, x2, x3, x4) = U21_gaa(x4)
U22_gaa(x1, x2, x3, x4) = U22_gaa(x4)
U23_gaa(x1, x2, x3, x4) = U23_gaa(x4)
U24_gaa(x1, x2, x3, x4) = U24_gaa(x4)
U25_gaa(x1, x2, x3, x4) = U25_gaa(x4)
U26_gaa(x1, x2, x3, x4) = U26_gaa(x4)
U27_gaa(x1, x2, x3, x4) = U27_gaa(x4)
U28_gaa(x1, x2, x3, x4) = U28_gaa(x4)
U29_gaa(x1, x2, x3) = U29_gaa(x3)
U30_gaa(x1, x2, x3) = U30_gaa(x3)
U31_gaa(x1, x2, x3) = U31_gaa(x3)
GOALF_IN_GAA(x1, x2, x3) = GOALF_IN_GAA(x1)
U13_GAA(x1, x2, x3, x4) = U13_GAA(x4)
S2TA_IN_GA(x1, x2) = S2TA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x4)
U2_GA(x1, x2, x3, x4) = U2_GA(x4)
U3_GA(x1, x2, x3, x4) = U3_GA(x4)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x4)
U15_GAA(x1, x2, x3, x4) = U15_GAA(x4)
PD_IN_GAAAA(x1, x2, x3, x4, x5) = PD_IN_GAAAA(x1)
U8_GAAAA(x1, x2, x3, x4, x5, x6) = U8_GAAAA(x6)
TAPPENDE_IN_GAAA(x1, x2, x3, x4) = TAPPENDE_IN_GAAA(x1)
U11_GAAA(x1, x2, x3, x4, x5) = U11_GAAA(x1, x5)
TAPPENDB_IN_GAA(x1, x2, x3) = TAPPENDB_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6) = U4_GAA(x3, x6)
U5_GAA(x1, x2, x3, x4, x5, x6) = U5_GAA(x1, x6)
U12_GAAA(x1, x2, x3, x4, x5) = U12_GAAA(x1, x5)
U9_GAAAA(x1, x2, x3, x4, x5, x6) = U9_GAAAA(x6)
U10_GAAAA(x1, x2, x3, x4, x5, x6) = U10_GAAAA(x4, x6)
TLASTC_IN_AG(x1, x2) = TLASTC_IN_AG(x2)
U6_AG(x1, x2, x3, x4, x5) = U6_AG(x5)
U7_AG(x1, x2, x3, x4, x5) = U7_AG(x5)
U16_GAA(x1, x2, x3, x4) = U16_GAA(x4)
U17_GAA(x1, x2, x3, x4) = U17_GAA(x4)
U18_GAA(x1, x2, x3, x4) = U18_GAA(x4)
U19_GAA(x1, x2, x3, x4) = U19_GAA(x4)
U20_GAA(x1, x2, x3, x4) = U20_GAA(x4)
U21_GAA(x1, x2, x3, x4) = U21_GAA(x4)
U22_GAA(x1, x2, x3, x4) = U22_GAA(x4)
U23_GAA(x1, x2, x3, x4) = U23_GAA(x4)
U24_GAA(x1, x2, x3, x4) = U24_GAA(x4)
U25_GAA(x1, x2, x3, x4) = U25_GAA(x4)
U26_GAA(x1, x2, x3, x4) = U26_GAA(x4)
U27_GAA(x1, x2, x3, x4) = U27_GAA(x4)
U28_GAA(x1, x2, x3, x4) = U28_GAA(x4)
U29_GAA(x1, x2, x3) = U29_GAA(x3)
U30_GAA(x1, x2, x3) = U30_GAA(x3)
U31_GAA(x1, x2, x3) = U31_GAA(x3)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GOALF_IN_GAA(s(T19), T13, T14) → U13_GAA(T19, T13, T14, s2tA_in_ga(T19, X31))
GOALF_IN_GAA(s(T19), T13, T14) → S2TA_IN_GA(T19, X31)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → U1_GA(T27, X66, X67, s2tA_in_ga(T27, X66))
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → U2_GA(T33, X96, X97, s2tA_in_ga(T33, X97))
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → U3_GA(T39, X126, X127, s2tA_in_ga(T39, X126))
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)
GOALF_IN_GAA(s(T19), T62, T63) → U14_GAA(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_GAA(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → PD_IN_GAAAA(T61, X168, T62, X167, T63)
PD_IN_GAAAA(T61, X168, T62, X167, T63) → U8_GAAAA(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
PD_IN_GAAAA(T61, X168, T62, X167, T63) → TAPPENDE_IN_GAAA(T61, X168, T62, X167)
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → U11_GAAA(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → TAPPENDB_IN_GAA(T100, T101, X252)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_GAA(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_GAA(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → U12_GAAA(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → TAPPENDB_IN_GAA(T189, T190, X364)
PD_IN_GAAAA(T61, T64, T62, T65, T66) → U9_GAAAA(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_GAAAA(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → TLASTC_IN_AG(T66, T65)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → U6_AG(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)
TLASTC_IN_AG(T236, node(T233, T234, T237)) → U7_AG(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
GOALF_IN_GAA(s(T244), T13, T14) → U16_GAA(T244, T13, T14, s2tA_in_ga(T244, X434))
GOALF_IN_GAA(s(T244), T264, T265) → U17_GAA(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_GAA(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, X465, T263), T264, X464)
GOALF_IN_GAA(s(T244), T264, T268) → U19_GAA(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_GAA(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, T266, T263), T264, T267)
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_GAA(T244, T264, T268, tlastC_in_ag(T268, T267))
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → TLASTC_IN_AG(T268, T267)
GOALF_IN_GAA(s(T275), T13, T14) → U22_GAA(T275, T13, T14, s2tA_in_ga(T275, X495))
GOALF_IN_GAA(s(T275), T295, T296) → U23_GAA(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_GAA(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, X527, nil), T295, X526)
GOALF_IN_GAA(s(T275), T295, T299) → U25_GAA(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_GAA(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, T297, nil), T295, T298)
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_GAA(T275, T295, T299, tlastC_in_ag(T299, T298))
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → TLASTC_IN_AG(T299, T298)
GOALF_IN_GAA(s(T306), T317, T318) → U28_GAA(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
GOALF_IN_GAA(s(T306), T317, T318) → PD_IN_GAAAA(nil, X569, T317, X568, T318)
GOALF_IN_GAA(0, T331, T332) → U29_GAA(T331, T332, tappendB_in_gaa(nil, T331, X588))
GOALF_IN_GAA(0, T331, T332) → TAPPENDB_IN_GAA(nil, T331, X588)
GOALF_IN_GAA(0, T331, T336) → U30_GAA(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_GAA(T331, T336, tlastC_in_ag(T336, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → TLASTC_IN_AG(T336, T335)

The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 46 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)

The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)

R is empty.
The argument filtering Pi contains the following mapping:
node(x1, x2, x3) = node(x1, x3)
TLASTC_IN_AG(x1, x2) = TLASTC_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TLASTC_IN_AG(node(T233, T237)) → TLASTC_IN_AG(T237)
TLASTC_IN_AG(node(T221, T219)) → TLASTC_IN_AG(T221)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TLASTC_IN_AG(node(T233, T237)) → TLASTC_IN_AG(T237)
The graph contains the following edges 1 > 1
TLASTC_IN_AG(node(T221, T219)) → TLASTC_IN_AG(T221)
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)

The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)

R is empty.
The argument filtering Pi contains the following mapping:
node(x1, x2, x3) = node(x1, x3)
TAPPENDB_IN_GAA(x1, x2, x3) = TAPPENDB_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TAPPENDB_IN_GAA(node(T171, T175)) → TAPPENDB_IN_GAA(T175)
TAPPENDB_IN_GAA(node(T159, T157)) → TAPPENDB_IN_GAA(T159)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TAPPENDB_IN_GAA(node(T171, T175)) → TAPPENDB_IN_GAA(T175)
The graph contains the following edges 1 > 1
TAPPENDB_IN_GAA(node(T159, T157)) → TAPPENDB_IN_GAA(T159)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)

The TRS R consists of the following rules:

goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
node(x1, x2, x3) = node(x1, x3)
nil = nil
S2TA_IN_GA(x1, x2) = S2TA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S2TA_IN_GA(s(T33)) → S2TA_IN_GA(T33)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

S2TA_IN_GA(s(T33)) → S2TA_IN_GA(T33)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPSizeChangeProof (EQUIVALENT transformation)

(29) YES